1. $\uparrow$tt
\\[0ex]$\vdash$  tt = tt